Would like a few more examples showing the use of assure alongside assert (namely, assert should be used for pre-conditions, and assure for post-condition invariants that should never be violated)

It may even be useful to have a few assert post-conditions (non-invariant checks) to show that assure is sort of a "last resort" mechanism used in only specific use cases.

@fubuloubu I am not that keen that we have 2 different asserts, and I still don't think having two types is a good idea (even more so because we have reason string support -> e.g. assert 1 != 2, "never"). So I would rather not advertise the use case, people that will want to use it will know how in any case. We don't currently have a examples for assert, so I don't think we should have examples on assure either then - people just pick it up and go a long.
If you would like to add a good documented section on assertion I am keen to read it and merge it, but to be honest I am probably not the right person to write it up.

Having thought about it some more. Scratch most of what I said above. I am actually OK with having the function, especially because of the tool support (invalid being the de facto).
I also think having support for what these tools/analyzers offer are great.
@fubuloubou - I am still keen on you writing the examples though, as I think you will write it better than myself.

Okay, I assigned myself to add documentation on this feature and how to use it effectively. Let's keep #711 open until that is complete.

Cool, thanks :) it's been a while since I have thought about the analyzers, do we still have that model checker issue somewhere?

It would be fantastic to get someone to review this new feature.

cc @maurelian @wuestholz @japesinator @montyly could you aid us?

@fubuloubu @jacqueswww Great to see this being added! In general, any solution that allows to distinguish between parameter validation (require in Solidity or REVERT in EVM) and properties that should (in principle) always hold (assert in Solidity and INVALID in EVM) will be very useful to developers and tool builders.

The ideal solution would probably be to change the semantics of the existing assert keyword to compile to the INVALID opcode and introduce a new require (or assume) keyword that is used for parameter validation (using REVERT). This would be in line with Solidity and less confusing to developers. I was actually involved in a similar discussion there (ethereum/solidity#1702) way back that led to the introduction of require.

On the other hand, I understand that you might not want to change the semantics and then your solution will work as long as it is well-documented.

@fubuloubu @wuestholz the main reason we didn't want to change assert is that Vyper is rooted in python. Where assert gets used for input validation, as well as test assertions, this is why the terminology was chosen as such in #711 - assert with revert is also the natural choice someone writing a contract should use by default (because of the gas refund). I think it makes sense to leave the naming as is (I remember discussing this at length regarding the positives and negatives of either - and then settling on the above.).

Meeting notes: closing in favour a proposal to be done where assure gets removed and assert <condition>, UNREACHABLE is used instead.

@maurelian @wuestholz @japesinator @montyly we've made a decision to modify the syntax to what @jacqueswww has proposed here: #711 (comment)

Please give us feedback!